T:Type{i}, L:T List, P:(TTProp{i'}). (x,yL.P(x,y))  Prop{i'} 

latex

Definitions	(x,yL.P(x;y)), x(s1,s2), l[i], x:A. B(x), {i..j}, i  j < k, AB, P & Q, A, False, P  Q, ||as||, Prop, t  T
Lemmas	select wf, int seg wf, length wf1